<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN"
"http://www.w3.org/TR/html4/loose.dtd">

<html>
<head>

<title>
PRISM Manual | PropertySpecification / SyntaxAndSemantics 
</title>

<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
<meta name="keywords" content="prism, probabilistic, symbolic, model, checker, verification, birmingham, oxford, parker, norman, kwiatkowska">

<link rel="icon" href="../pub/skins/offline/images/p16.ico" type="image/x-icon">
<link rel="shortcut icon" href="../pub/skins/offline/images/p16.ico" type="image/x-icon">

<!--HTMLHeader--><style type='text/css'><!--
  ul, ol, pre, dl, p { margin-top:0px; margin-bottom:0px; }
  code.escaped { white-space: nowrap; }
  .vspace { margin-top:1.33em; }
  .indent { margin-left:40px; }
  .outdent { margin-left:40px; text-indent:-40px; }
  a.createlinktext { text-decoration:none; border-bottom:1px dotted gray; }
  a.createlink { text-decoration:none; position:relative; top:-0.5em;
    font-weight:bold; font-size:smaller; border-bottom:none; }
  img { border:0px; }
  .editconflict { color:green; 
  font-style:italic; margin-top:1.33em; margin-bottom:1.33em; }

  table.markup { border:2px dotted #ccf; width:90%; }
  td.markup1, td.markup2 { padding-left:10px; padding-right:10px; }
  table.vert td.markup1 { border-bottom:1px solid #ccf; }
  table.horiz td.markup1 { width:23em; border-right:1px solid #ccf; }
  table.markup caption { text-align:left; }
  div.faq p, div.faq pre { margin-left:2em; }
  div.faq p.question { margin:1em 0 0.75em 0; font-weight:bold; }
  div.faqtoc div.faq * { display:none; }
  div.faqtoc div.faq p.question 
    { display:block; font-weight:normal; margin:0.5em 0 0.5em 20px; line-height:normal; }
  div.faqtoc div.faq p.question * { display:inline; }
   
    .frame 
      { border:1px solid #cccccc; padding:4px; background-color:#f9f9f9; }
    .lfloat { float:left; margin-right:0.5em; }
    .rfloat { float:right; margin-left:0.5em; }
a.varlink { text-decoration:none; }

.sourceblocklink {
  text-align: right;
  font-size: smaller;
}
.sourceblocktext {
  padding: 0.5em;
  border: 1px solid #808080;
  color: #000000;
  background-color: #f1f0ed;
}
.sourceblocktext div {
  font-family: monospace;
  font-size: small;
  line-height: 1;
  height: 1%;
}
.sourceblocktext div.head,
.sourceblocktext div.foot {
  font: italic medium serif;
  padding: 0.5em;
}

--></style>  <meta name='robots' content='index,follow' />


<link type="text/css" rel="stylesheet" href="../pub/skins/offline/css/base.css">
<link type="text/css" rel="stylesheet" href="../pub/skins/offline/css/prism.css">
<link type="text/css" rel="stylesheet" href="../pub/skins/offline/css/prismmanual.css">

</head>

<body text="#000000" bgcolor="#ffffff">

<div id="layout-maincontainer">
<div id="layout-main">

<div id="prism-mainbox">

<!-- ============================================================================= -->

<!--PageHeaderFmt-->
<!--/PageHeaderFmt-->

<!--PageTitleFmt-->
  <div id="prism-man-title">
    <p><a class='wikilink' href='Introduction.html'>Property Specification</a> /
</p><h1>Syntax And Semantics</h1>

  </div>
<!--PageText-->
<div id='wikitext'>
<h3>Syntax</h3>
<p>The syntax of the PRISM property specification language subsumes various probabilistic temporal logics, including PCTL, CSL, LTL and PCTL*. Informally, the syntax can be summarised as follows: a property can be any valid, well-typed PRISM <a class='wikilink' href='../ThePRISMLanguage/Expressions.html'>expression</a>, which (optionally) also includes the three probabilistic operators just discussed (<code><strong>P</strong></code>, <code><strong>S</strong></code> and <code><strong>R</strong></code>). This mean that any of the following operators can be used:
</p>
<div class='vspace'></div><ul><li><code>-</code> (unary minus)
</li><li><code>*</code>, <code>/</code> (multiplication, division)
</li><li><code>+</code>, <code>-</code> (addition, subtraction)
</li><li><code>&lt;</code>, <code>&lt;=</code>, <code>&gt;=</code>, <code>&gt;</code> (relational operators)
</li><li><code>=</code>, <code>!=</code> (equality operators)
</li><li><code>!</code> (negation)
</li><li><code>&amp;</code> (conjunction)
</li><li><code>|</code> (disjunction)
</li><li><code>&lt;=&gt;</code> (if-and-only-if)
</li><li><code>=&gt;</code> (implication)
</li><li><code>?</code> (condition evaluation: <code>condition ? a : b</code> means "if <code>condition</code> is true then <code>a</code> else <code>b</code>")
</li><li><code><strong>P</strong></code> (probabilistic operator)
</li><li><code><strong>S</strong></code> (steady-state operator)
</li><li><code><strong>R</strong></code> (reward operator)
</li></ul><p class='vspace'>This allows you to write any property expressible in logics such as PCTL and CSL. For example, CSL allows you to nest <code><strong>P</strong></code> and <code><strong>S</strong></code> operators:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock1'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>=? [ <span class="prismkeyword">F</span>&gt;<span class="prismnum">2</span> <span class="prismkeyword">S</span>&gt;<span class="prismnum">0.9</span>[ <span class="prismident">num_servers</span> &gt;= <span class="prismnum">5</span> ] ]<br/>
</div></div>
  <div class='sourceblocklink'><a href='SyntaxAndSemantics@action=sourceblock&amp;num=1' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>"the probability of it taking more than 2 hours to get to a state from which the long-run probability of at least 5 servers being operational is &gt;0.9"
</p>
<p class='vspace'>You can also express various arithmetic expressions such as:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock2'>
  <div class='sourceblocktext'><div class="prism"><span class="prismnum">1</span> - <span class="prismkeyword">P</span>=? [ <span class="prismkeyword">F</span>[<span class="prismnum">3600</span>,<span class="prismnum">7200</span>] <span class="prismident">oper</span> ]<br/>
</div></div>
  <div class='sourceblocklink'><a href='SyntaxAndSemantics@action=sourceblock&amp;num=2' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>"the probability that the system is <strong>not</strong> operational at any point during the second hour of operation"
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock3'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">R</span>{"<span class="prismident">oper</span>"}=? [ <span class="prismkeyword">C</span>&lt;=<span class="prismident">t</span> ] / <span class="prismident">t</span><br/>
</div></div>
  <div class='sourceblocklink'><a href='SyntaxAndSemantics@action=sourceblock&amp;num=3' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>"the expected fraction of time that the system is available (i.e. the expected interval availability) in the time interval [0, t]"
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock4'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>=? [ <span class="prismkeyword">F</span> <span class="prismident">fail_A</span> ] / <span class="prismkeyword">P</span>=? [ <span class="prismkeyword">F</span> <span class="prismident">any_fail</span> ]<br/>
</div></div>
  <div class='sourceblocklink'><a href='SyntaxAndSemantics@action=sourceblock&amp;num=4' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>"the (conditional) probability that component A eventually fails, given
that at least one component fails"
</p>
<div class='vspace'></div><h3>Semantics</h3>
<p>We omit a formal presentation of the semantics of the PRISM property language. The semantics of the probabilistic temporal logics that the language incorporates can be found from a variety of sources. See for example the pointers given in the <a class='urllink' href='http://www.prismmodelchecker.org/about.php'>About</a> and <a class='urllink' href='http://www.prismmodelchecker.org/doc/'>Documentation</a> sections of the PRISM website.
</p>
<p class='vspace'>It is worth, however, clarifying a few points specific to PRISM. A property is evaluated with respect to a particular state of a model. Depending on the type of the property, this value may either be a Boolean, an integer or a double. When performing model checking, PRISM usually has to actually compute the value for <em>all</em> states of the model but, for clarity, will by default report just a single value. Typically, this is the value for the (single) initial state of the model. For example, this:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock5'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>=? [ <span class="prismkeyword">F</span> "<span class="prismident">error</span>" ]<br/>
</div></div>
  <div class='sourceblocklink'><a href='SyntaxAndSemantics@action=sourceblock&amp;num=5' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>will report the probability, from the initial state of the model, of reaching an "error" state.
This:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock6'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>&gt;<span class="prismnum">0.5</span> [ <span class="prismkeyword">F</span> "<span class="prismident">error</span>" ]<br/>
</div></div>
  <div class='sourceblocklink'><a href='SyntaxAndSemantics@action=sourceblock&amp;num=6' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>will return <code>true</code> if and only if the probability, from the initial state, is greater than 0.5.
</p>
<p class='vspace'><strong>Note:</strong> This is contrast to older versions of PRISM, which treated numerical and Boolean-valued properties differently in this respect.
</p>
<p class='vspace'>For models with <a class='wikilink' href='../ThePRISMLanguage/MultipleInitialStates.html'>multiple initial states</a>, we need to adapt these definitions slightly. In this case, the two properties above will yield, respectively:
</p>
<div class='vspace'></div><ul><li>the range of values (over all initial states) of the probability of reaching "error"
<div class='vspace'></div></li><li><code>true</code> if and only if the probability is greater than 0.5 from <em>all</em> initial states.
</li></ul><p class='vspace'>You can also ask PRISM to return different values using <a class='wikilink' href='Filters.html'>filters</a>,
which are described in the next section.
</p>
</div>


<!--PageFooterFmt-->
  <div id='prism-man-footer'>
  </div>
<!--/PageFooterFmt-->


<!-- ============================================================================= -->

</div> <!-- id="prism-mainbox" -->

</div> <!-- id="layout-main" -->
</div> <!-- id="layout-maincontainer" -->

<div id="layout-leftcol">
<div id="prism-navbar2">

<h3><a class='wikilink' href='../Main/Welcome.html'>PRISM Manual</a></h3>
<p><strong><a class='wikilink' href='Introduction.html'>Property Specification</a></strong>
</p><ul><li><a class='wikilink' href='Introduction.html'>Introduction</a>
</li><li><a class='wikilink' href='IdentifyingASetOfStates.html'>Identifying A Set Of States</a>
</li><li><a class='wikilink' href='ThePOperator.html'>The P Operator</a>
</li><li><a class='wikilink' href='TheSOperator.html'>The S Operator</a>
</li><li><a class='wikilink' href='Reward-basedProperties.html'>Reward-based Properties</a>
</li><li><a class='selflink' href='SyntaxAndSemantics.html'>Syntax And Semantics</a>
</li><li><a class='wikilink' href='Filters.html'>Filters</a>
</li><li><a class='wikilink' href='PTAProperties.html'>PTA Properties</a>
</li><li><a class='wikilink' href='PropertiesFiles.html'>Properties Files</a>
</li></ul><p>[ <a class='wikilink' href='AllOnOnePage.html'>View all</a> ]
</p>


</div>  <!-- id="prism-navbar2" -->
</div> <!-- id="layout-leftcol" -->

</body>
</html>
